T:Type, l:(T List), x, y:T. no_repeats(T;l)  x before y  l  (y before x  l) 

latex

ProofTree

Definitions	t  T, A, x before y  l, P  Q, x:A. B(x), , {T}, P & Q, P  Q, Y, as @ bs, P  Q, P  Q, False
Lemmas	no repeats wf, sublist wf, sublist transitivity, sublist weakening, cons sublist cons, append overlapping sublists, no repeats iff